STM: first wf

ABS: pred(e)

STM: pred wf

ABS: ecase1(e;info;i.f(i);l,e'.g(l;e'))

STM: ecase1 wf

ABS: loc(e)

STM: loc wf

ABS: rcv?(e)

STM: rcv? wf

ABS: sender(e)

STM: sender wf

ABS: link(e)

STM: link wf

ABS: pred!(e;e')

STM: pred! wf

STM: pred-total

ABS: e < e'

STM: cless wf

STM: cless-eq-loc

ABS: sends-bound(p;e;l)

STM: sends-bound wf

STM: sends-bound-property

STM: strong-sends-bound-property

STM: pred-first-lemma

ABS: eventlist(pred?;e)

STM: eventlist wf

STM: member eventlist

STM: l before eventlist

STM: l before eventlist iff

ABS: rcv-from-on(dE;dL;info;e;l;r)

STM: rcv-from-on wf

STM: assert-rcv-from-on

ABS: receives(dE;dL;pred?;info;p;e;l)

STM: receives wf

STM: member receives

ABS: index(dE;dL;pred?;info;p;r)

STM: index wf

STM: index-property1

ABS: kind(e)

STM: kind wf

ABS: rtag(info;e)

STM: rtag wf

STM: rcv?-kind

STM: rcv?-link

ABS: EOrderAxioms(E; pred?; info)

STM: EOrderAxioms wf

ABS: EState(T)

STM: EState wf

ABS: s+r

STM: es-shift wf

ABS: when-after(e;info;pred?;init;Trans;val;time)

STM: when-after wf

ABS: state_when(e)

STM: state when wf

ABS: state_after(e)

STM: state after wf

ABS: val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time)

STM: val-axiom wf

ABS: rmsg(info;val;e)

STM: rmsg wf

ABS: sends(dE;dL;pred?;info;val;p;e;l)

STM: sends wf

STM: better-sends wf

ABS: SESAxioms{i:l}(E;T;pred?;info;when;after;time)

STM: SESAxioms wf

ABS: eventtype(k;loc;V;M;e)

STM: eventtype wf

ABS: ESAxioms{i:l}(E;T;M;loc;kind;val;when;after;time;sends;sender;index;first;pred;causl)

STM: ESAxioms wf

STM: SES-implies-ES

ABS: constant_function(f;A;B)

STM: constant function wf

ABS: ES

STM: event system wf

ABS: E

STM: es-E wf

ABS: es-eq(es)

STM: es-eq wf

ABS: es-pred?(es)

STM: es-pred? wf

ABS: es_info(es)

STM: es info wf

ABS: loc(e)

STM: es-loc wf

ABS: kind(e)

STM: es-kind wf

ABS: es-oaxioms(es)

STM: es-oaxioms wf

ABS: es-T(es)

STM: es-T wf

ABS: es-V(es)

STM: es-V wf

ABS: es-M(es)

STM: es-M wf

ABS: discrete(i;x)

STM: es-isconst wf

ABS: Msg

STM: es-Msg wf

ABS: (Msg on l)

STM: es-Msgl wf

ABS: isrcv(e)

STM: es-isrcv wf

ABS: tag(e)

STM: es-tag wf

ABS: lnk(e)

STM: es-lnk wf

ABS: act(e)

STM: es-act wf

ABS: rcvtype(e)

STM: es-rcvtype wf

ABS: acttype(e)

STM: es-acttype wf

ABS: kindtype(i;k)

STM: es-kindtype wf

ABS: valtype(e)

STM: es-valtype wf

ABS: es_vartype(es;i;x)

STM: es vartype wf

ABS: vartype(i;x)

STM: es-vartype wf

ABS: es_state(es;i)

STM: es state wf

STM: es-shift wf2

ABS: state@i

ABS: state@i|xs

STM: es-partial-state wf

STM: es-state wf

STM: es-state-subtype-partial-state

ABS: s.x

STM: es-state-ap wf

ABS: es_init(es)

STM: es init wf

ABS: x initially@i 

STM: es-initially wf

ABS: initial state @i

STM: es-init-state wf

ABS: s(now)

STM: es-read-state wf

ABS: es-Trans(es)

ABS: es_val(es)

STM: es val wf

STM: es-Trans wf

ABS: es-Send(es)

STM: es-Send wf

ABS: es-Choose(es)

STM: es-Choose wf

ABS: first(e)

STM: es-first wf

STM: can-apply-pred?

ABS: pred(e)

STM: es-pred wf

STM: do-apply-pred?

ABS: es-pred!(es;e;e')

STM: es-pred! wf

STM: es-loc-pred

STM: es-loc-pred-plus

STM: es-pred!-wellfounded

ABS: val(e)

STM: es-val wf

ABS: time(e)

STM: es-time wf

ABS: es_time(es)

STM: es time wf

ABS: es_state_when(es;e)

STM: es state when wf

ABS: (timed)state after e

STM: es state after wf

ABS: (state when e)

ABS: state after e

ABS: x when e

STM: es-when wf

STM: es-state-when wf

ABS: (x after e)

STM: es-after wf

STM: es-state-after wf

ABS: sends(l;e)

STM: es-sends wf

ABS: sender(e)

STM: es-sender wf

ABS: index(e)

STM: es-index wf

ABS: (e < e')

STM: es-causl wf

ABS: (e <loc e')

STM: es-locl wf

ABS: e loc e' 

STM: es-le wf

ABS: Trans(i)

STM: es-trans wf

ABS: Send(i)

STM: es-send wf

ABS: Choose(i)

STM: es-choose wf

STM: es-axioms

STM: es-locl-wellfnd

STM: es-discrete-const

STM: es-isconst-property

STM: es-locl-antireflexive

STM: es-locl irreflexivity

STM: es-le-loc

STM: es-locl-iff

STM: es-dst-lnk

ABS: mtag(m)

STM: es-mtag wf

ABS: s1  s2 mod x@i

STM: es-x-equiv wf

ABS: es-independent(es;i;k;x)

STM: es-independent wf

STM: mlnk wf2

ABS: sends(l,tg,e)

STM: es-tg-sends wf

ABS: State(ds)

STM: decl-state wf

STM: decl-state-eta

ABS: e@i. P(e)

STM: alle-at wf

STM: es-rcv-kind

STM: es-kind-rcv

ABS: e'e.P(e')

STM: existse-ge wf

ABS: @i state ds

STM: es-state-type wf

STM: es-state-type-implies

ABS: DeclaredType(ds;x)

STM: decl-type wf

ABS: @i(x:T)

STM: es-dtype wf

ABS: @i x initially v:T

STM: init-p wf

ABS: @i continuous x initially v:T

STM: init p wf

STM: init p-discrete

ABS: @i only events in L change   x : T

STM: frame-p wf

ABS: only events in L send on l with tg

STM: sframe-p wf

ABS: @i: k affects only L

STM: aframe-p wf

ABS: @i:k sends only on links in L

STM: bframe-p wf

ABS: @i:k sends only on links in L

STM: kind-send-frame wf

ABS: @i: only members of L read x

STM: rframe-p wf

ABS: @i events of kind k change x to f State(ds) (val:T)

STM: effect-p wf

ABS: @i events of kind k change continuous x to f State(ds) (val:T)

STM: effect p wf

STM: effect p-discrete

ABS: rcvs from e on l = L

STM: es-rcv-from wf

ABS: loc-ordered(es;L)

STM: loc-ordered wf

STM: loc-ordered-equality

ABS: es-receives(es;e;l)

STM: es-receives wf

STM: member-es-receives

STM: loc-ordered-es-receives

STM: es-rcv-from-equal-receives

STM: es-rcv-from-member-index

STM: es-rcv-from-implies

ABS: sends-msgs(s;v;tg_f)

STM: sends-msgs wf

ABS: sends k(v:T) on l:tagged(g,State(ds),v):dt

STM: sends-p wf

ABS: (state after e)+t

STM: es-state-after-elapsed wf

STM: discrete-after-elapsed

ABS: (initial state @ i)+t

STM: es-init-elapsed wf

STM: discrete-init-elapsed

ABS: es-kind-index(es;k;e)

STM: es-kind-index wf

ABS: @i Precondition for a:Outcome(p) is P:State(ds) 

STM: pre-p wf

STM: es-time-order